1. Field of the Invention
This invention relates to a program, an apparatus and a method for verifying a program that verifies a concurrent program or a parallel program.
2. Description of the Related Art
A concurrent program or a parallel program is composed of a plurality of processes (threads). The processes may refer to and/or rewrite a shared same resource (common variable). However, when a plurality of processes is allowed to freely refer to and/or rewrite shared resources, a result that the program designer did not expect can be output by the program.
Now, a parallel program will be described by way of a specific example. The parallel program of this example is composed of a definition of shared variable “shared”, a function “Process 01” and another function “Process 02”. In the accompanying drawings, FIG. 32 illustrates a source code that is an example of definition of a shared variable in a parallel program while FIG. 33 illustrates a source code that is an example of function Process 01 and FIG. 34 illustrates a source code that is an example of function Process 02. The two processes Process 01 and Process 02 share a shared variable “shared”. The parallel program is specified in such a way that the function Process 01 and the function Process 02 operate in parallel and functions a(1) and b(0) are invoked alternately. For example, a trace as described below can take place as that of a first parallel program.    1. Process 01. Refer to shared (shared==0)    2. Process 01. shared=1    3. Process 02. Refer to shared (shared==1)    4. Process 02. shared=0    5. Process 02. b (0)    6. Process 01. a (0)
The trace of this example is a has an error because the order of the execution of the function a and that of the function b is inverted and the both arguments become equal to 0 and do not meet the specified requirements.
A synchronizing mechanism such as MUTEX lock or semaphore is used to prevent such a problem. For example, programs can be modified by using a MUTEX lock. When a process refers or writes to a shared resource, using a synchronizing mechanism, the designed execution order is observed because another process does not interfere with it. FIG. 35 illustrates a source code that shows an example of result of modification of the function Process 01 in the parallel program. FIG. 36 illustrates a source code that shows an example of result of modification of the function Process 02 in the parallel program. In this example, the parts protected by lock l (from a call for locking and a call for unlocking) are sequentially executed.
For example, the technique that is described in Patent Document 1 (Japanese Patent Application Laid-Open Publication No. 8-328897) is known as a related conventional technique. The parallel program operation analysis method described in the above patent document is designed to display the state of transition of each of the parallel programs that operate on a parallel computer and support the effort of identifying the cause of the error, if any.
However, the number of the parts that are executed sequentially increases when a synchronizing mechanism as described above is put to use frequently. Then, the merit of the parallelism of programs will not be exploited satisfactorily. Such a situation is not desirable from the viewpoint of performance. Additionally, the operation of the synchronizing mechanism involves overhead, which by turn further reduces the performance.
However, many concurrent/parallel programs are executed on assumptions. Therefore, the load of synchronous operations can be partly alleviated when the programs are altered by taking the assumptions into consideration. Then, as the load of synchronous operations is alleviated, the time that can be spent for executing processes concurrently or in parallel is increased to improve the speed of execution of the entire programs. However, to improve the speed of execution of concurrent or parallel programs so as to make them operate properly, it is necessary to conduct the job of improving the speed of execution while comparing the outcome of the programs before the alterations and that of the programs after the alterations. Then, an interactive tool such as debugger is required for the job. Particularly, it is a difficult job to identify the error that is caused by synchronism of concurrent/parallel programs.
In the case of a debugger for ordinary serial programs, test data are selected in advance for the program to be debugged and the designer executes each step, observing the outcome of execution of the step. In the case of concurrent or parallel programs, the outcome of execution depends not only on the test data but also on the timing of accessing the shared resource of each process. However, debuggers for ordinary serial programs are not designed by taking such timings into consideration, therefore they are not suited for debugging concurrent/parallel programs.
Debuggers specifically designed for concurrent/parallel programs are available. Such debuggers adopt a technique of feeding test data, altering the timings of execution of processes that operate concurrently or in parallel. However, since all the timings of execution of processes have to be tested with such a technique, a very long time will have to be spent for debugging.
Additionally, formal verification techniques such as a model check technique are employed for debugging concurrent/parallel programs. An ordinary model check technique proceeds in a manner as described below. A model of an entire program that operates properly before an alteration such as a FSM (finite state machine) is prepared in advance. After the alteration of the program, a model of the altered program is prepared and the two models are compared by means of an equivalence verification technique or a similar technique. However, when in the case of a large scale program, the operation of preparing such a model is very time consuming and that of preparing models is also very time consuming. Therefore, the operation of interactively debugging an ordinary program has been a difficult one.